COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	macro.lsp[w82,jmc]	ekl programs for doing induction
C00004 ENDMK
C⊗;
macro.lsp[w82,jmc]	ekl programs for doing induction

(defun startsexpind (phi simplines sortlines)
       (prog ()
	     (setq ssortlines sortlines)
	     (assume '(atom x))
	     (setq atomassume *)
	     (assume (etrw (list phi '(car x)) nil sortlines))
	     (setq carassume *)
	     (assume (etrw (list phi '(cdr x)) nil sortlines))
	     (setq cdrassume *)
))

(defun endsexpind (phi atomconc carcdrconc)
       (prog ()
	     (ecases (list 'or atomassume carassume cdrassume)
		     (list atomconc carconc cdrconc))
	     (e∀i '((x x)) *)
	     (e∀e
	      (list phi)
	      sexpinduction
	      (list nil (list $ -1))
	      ssortlines 
	      nil)
))